6.5 KB · ⇊ 2 parts · ⤓ Micron 6.5 KB · ⤓ HTML 14.8 KB

top

Der Begriff Formale Methode bezeichnet in der Informatik eine Vielzahl von natur- und ingenieurswissenschaftlichen Techniken zur Modellierung und mathematisch rigorosen Überprüfung von Computersystemen. Die Anwendung von Formalen Methoden zur Analyse von Software und Hardware ist motiviert von der Erwartung, dass wie in anderen ingenieurswissenschaftlichen Disziplinen eine angemesse mathematische Analyse zur Zuverlässigkeit und zur Stabilität eines Systems beitragen kann.

Formale Methoden bauen auf einer sehr breiten Basis von Konzepten aus der Theoretischen Informatik auf, wie z. B. Logik, Formale Sprachen, Automatentheorie, Formale Semantik und Typsysteme.

• Relevanz

• Siehe auch

• Weblinks

• Einzelnachweise

Formale Methoden erleben in den letzten Jahren einen Aufschwung. Statische Programmanalyse wird zum Beispiel bei Airbuscite-ref-1[1] und Microsoft verwendet. Microsoft selbst unterhält bei Microsoft Research einige Forschungsgruppen, die sich mit formalen Methoden beschäftigen, und z. B. Treiber werden regelmäßig mit formalen Methoden überprüftcite-ref-2[2]. Amazon setzt im Bereich von Web Services auch auf formale Methodencite-ref-3[3]. Auch Google zeigt daran Interessecite-ref-4[4]. Es gibt eine Konferenz, die sich nur mit diesem Thema beschäftigtcite-ref-5[5].

Auch unter den Turing-Award-Gewinnern finden sich einige Forscher aus dem Bereich der formalen Methoden, z. B. Tony Hoare für seinen Beitrag zur formalen Spezifikation von Programmiersprachen, Robin Milner für seine allgemeine Theorie der Nebenläufigkeit, Amir Pnueli für seinen Beitrag zur temporalen Logik und Edmund M. Clarke, E. Allen Emerson und Joseph Sifakis für ihren Beitrag zum Model Checking.

• Formale Semantik

• Formale Spezifikation

• Formale Verifikation

• Theorembeweisen

• Modellprüfverfahren (model checking)

• Peter Padawitz: Formale Methoden des Systementwurfs. Dortmund 2010 (tu-dortmund.de [PDF] Vorlesungsskript).

• Christel Baier, Joost-Pieter Katoen: Principles of model checking. MIT press, 2008.

cite-note-11. ↑ Jean Souyris: Industrial Experience of Abstract Interpretation-Based Static Analyzers. In: Building the Information Society (= IFIP International Federation for Information Processing). Springer US, Boston, MA 2004, ISBN 978-1-4020-8157-6, S. 393–400, doi:10.1007/978-1-4020-8157-6_31 (springer.com [abgerufen am 20. April 2020]).

cite-note-22. ↑ SLAM. In: Microsoft Research. Abgerufen am 20. April 2020 (amerikanisches Englisch).

cite-note-33. ↑ Byron Cook: Formal Reasoning About the Security of Amazon Web Services. In: Computer Aided Verification (= Lecture Notes in Computer Science). Springer International Publishing, Cham 2018, ISBN 978-3-319-96145-3, S. 38–47, doi:10.1007/978-3-319-96145-3_3 (springer.com [abgerufen am 20. April 2020]).

cite-note-44. ↑ Edward Aftandilian, Raluca Sauciuc, Siddharth Priya, Sundaresan Krishnan: Building Useful Program Analysis Tools Using an Extensible Java Compiler. 2012, abgerufen am 20. April 2020 (englisch).

cite-note-55. ↑ Formal Methods in Industry. In: floc2018.org. Abgerufen am 20. April 2020 (amerikanisches Englisch).